i:Id, L:Knd List, x:Id, t:Type. @i: only L affects x : t  Dsys 

latex

Definitions	Dsys, @i: only L affects x : t, if b t else f fi, eqof(d), IdDeq, MsgA, only members of L affect x :t, x:A. B(x), , Knd, t  T, Id
Lemmas	Id wf, Knd wf, ma-empty wf, ma-single-frame wf, msga wf, id-deq wf, eqof wf, ifthenelse wf